A:Type, es:ES, I:AbsInterface(A), P:(E), p:(e:E. Dec(P(e))), e:E.
((e  (I|p)))  (((e  I)) & (P(e))) 

latex

Definitions	x:A. B(x), P & Q, b, f(a), x(s), A, x:A  B(x), P  Q, P  Q, P  Q, Type, t  T, Top, x:AB(x), S  T, left + right, E, suptype(S; T), can-apply(f;x), , Void, x:A.B(x), x.A(x), x. t(x), p-co-restrict(f;p), ES, Dec(P), e  X, (I|p), AbsInterface(A)
Lemmas	decidable wf, es-E wf, event system wf, iff functionality wrt iff, can-apply-p-co-restrict, p-co-restrict wf, top wf, can-apply wf, assert wf, not wf